Ja, herzlich willkommen.

Ja, also wie versprochen heute also der Beweis der starken Normalisierung in System F.

Ja, also wir machen das folgender Maßen, also das folgt klassischen Beweisen natürlich,

gira unter anderem, die Version, die wir hier machen, die ist gleich aus dem Bahrendrecht, wenn ich mich recht in Sinne... also wir machen das, indem wir so eine Art Semantik angeben für System F.

Das wird jetzt keine richtige, syntaxunabhängige denotationale Semantik, wie wir sie ja im Wesentlichen kennengelernt haben für Datentypen und so was, wo wir also sagen,

Datentypen entsprechen über Algebren, entsprechen Algebren und Algebren sind halt Mengen mit einer bestimmten Struktur und so was.

Das kriegt man für System F nur sehr schwer hin, weil einfach diese allquantifizierten Typen sind mit Mengentheorie im Wesentlichen inkompatibel,

es sei denn, man lässt sich auf sehr originelle, konstruktive Mengenlernen ein.

Da gibt es also zwei berühmte Papiere, einer ist von John Reynolds, Polymorphism is not set theoretic und eins von Andy Pitts, das heißt Polymorphism is set theoretic constructively.

Ja, das ist also alles jenseits dessen, was wir hier abhandeln können, aber wir haben eben so eine Art Pseudo-Semantik.

Pseudo-Semantik heißt, naja, wir weisen schon irgendwie einem Typen eine Menge zu, wir machen aber gleich so ein festes, syntaktisches Modell.

Und zwar weisen wir so einem Typen, Alpha, so eine Menge Semantik von Alpha zu.

Und zwar ist diese Semantik einfach eine Teilmenge der Menge Sn, wobei Sn aus allen Lambda-Termen T besteht, wo für die gilt T ist stark normalisieren.

Sieht doch aus einer zirkulären Definition aus, gut, das liegt eben daran, dass wir schon wissen, was stark normalisierend heißt.

Also stark normalisierend ist ein Lambda-Term dann, wenn er keine unendlichen Reduktionssequenzen hat.

So, also, es enden wir die Menge aller dieser stark normalisierenden Terme und jeden Typ weisen wir zu eine Teilmenge dieser Menge von Termen.

Das ist natürlich noch nicht die ganze Wahrheit, denn der Typ kann ja freie Typvariablen enthalten und wir wissen zunächst mal nicht, was wir mit denen matten sollen.

So, das heißt, genauer gesagt hängt das also ab von einem zusätzlichen Parameter Xi.

Und Xi spielt dieselbe Rolle wie eben die Umgebung bei einem normalen Termen mit freien Variablen.

Da müssen wir eben auch sagen, was ist die Bedeutung der freien Variablen.

Hier sind es die freien Typvariablen.

Entsprechend nennen wir Xi eine Typumgebung.

Und das ist eine Abbildung von, Tippfehler.

Eine Abbildung von unserer Menge V, Vfett gedruckt oder V an der Tafel der Typvariablen in, okay, jetzt eine bestimmte Menge möglicher Interpretationen für Typvariablen.

Und zwar nennen wir die Sat, wobei das hier die Menge der saturierten Teilmengen von Sn ist, wobei was saturiert nun heißt, wir demnächst noch definieren.

Also es ist eine bestimmte Teilmenge der Menge aller Teilmengen von Sn.

Das heißt, wir verlangen bestimmte Abschlusseigenschaften missermaßen von den Interpretationen der Typvariablen.

So, möchte ich nochmal das hier, ist die Menge der Lambda-Termen, dieses Groß-Lambda.

Achtung, Groß-Lambda hieß auch schon mal was anderes, nicht?

Also in Kapitel über Automaten war Groß-Lambda die Menge aller Sprachen.

Jetzt sind wir wieder im Lambda-Kalkül, da ist Groß-Lambda die Menge aller Lambda-Termen.

So, und dann zeigen wir, davon haben wir zunächst mal nichts, wir haben halt die Typen irgendwie interpretiert, wir wollen ja das über die Terme wissen, also nicht über die Typen.

Also wir wollen, dass alle in Lambda-2 typisierbaren Terme terminieren.

So, wir zeigen dann etwas, das ist einfach Korrektheit über diesem Modell, wenn man will.

Ich schreibe das mal salopp ohne Kontext, ach nee, falsch rum.

Wenn ein Term einen gewissen Typ hat, Alpha, dann ist der auch da drin.

So, ich lasse jetzt alles an Kontext und so weiter weg, das ist also extra saloppisch Schreibweise, alles nur um klar zu machen, wo es nachher langgeht, korrekte Schreibweisen kommen gleich.

Also jeder Term, der mit einem bestimmten Typ typisierbar ist, gehört auch zur Interpretation dieses Typs.

So, das ist also einfach nur Korrektheit gewissermaßen unseres Typisierungssystems über diesem Modell.

So, was haben wir davon?

Nun, wir haben alles davon, denn die Semantik von Typen besteht ja jeweils aus stark normalisierenden Termen.

Also jeder Term, der in der Semantik seines Typs liegt, ist stark normalisiert.

Also sobald wir das geschafft haben, haben wir gewonnen.

Das ist also jetzt hier unsere grobe Strategie.

So, jetzt mal zur Absetzung.

Ja, also das war der grobe Überblick mit lauter nicht wirklich definierten Begriffen.

Ab jetzt machen wir die korrekte technische Entwicklung.

Also, fangen wir an damit, wie wir dann aus dem Xi die Interpretation von dem Alpha gewinnen.

So, der Schlüssel dabei wird sein, die Interpretation der Funktionenräume.

So, wir gehen uns also jetzt mal her.